$P$ holds in state ${\it init}$ $\Rightarrow$ $\exists$e@$i$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\exists$$v$:$T$. $P$(($\lambda$$x$.${\it init}$($x$)?$\cdot$),$v$)) $\Rightarrow$ ($\exists$$e$:E. loc($e$) $=$ $i$)